(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun d () Real)
(declare-fun aa () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun ab () Real)
(declare-fun ac () Real)
(declare-fun ad () Real)
(declare-fun g () Real)
(declare-fun h () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun k () Real)
(declare-fun l () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun v () Real)
(declare-fun ep () Real)
(declare-fun p () Real)
(declare-fun ae () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(assert (forall ((af Real)) (=> (and (or (or (or (and (and (or (and (and (and (and (and (= o 0.0 (- aa)) (= (+ aa q) 2.0)) (= (- e) 2.0)) (>= 0 ac)) (= (/ 14 f ae) 2.0)) (<= o 0)) (< 0.0 (/ 14 b q))) (> 0.0 a)) (< (* n) v (/ 5 d j))) (<= (* c (- 5 d)) v)) (<= 0.0 h)) (< 0.0 v)) (>= 0.0 ep)) (or (= 0 ad) (<= 0.0 g) (<= af g) (or (or (or (<= 0.0 (/ 8 ab p)) (< p v)) (< 0.0 (/ (* h af) j))) (> (+ (+ h af) j) v)) (<= (- af) ep)) (= m 2.0))))
(assert (distinct c (* i ae)))
(assert (= aa (/ 78 k q)))
(assert (= e (* l q)))
(assert (= ab (/ v r)))
(check-sat)
